--- Test case for 'https://github.com/Frege/frege/issues/277 Issue 277'
{--
    > frege.runtime.Undefined: Can't adapt
    > Bind {a → a, Func.U<𝓐, 𝓐>, RunTM.<Func.U<CData<𝓐>, Func.U<𝓐, 𝓐>>>cast(arg$1)
    >                            .apply(Thunk.<CData<𝓐>>lazy(ctx$1)).call()}
    > to  Func.U<CData<Object>, Func.U<Object, Object>>
    > because  𝓐  does not match  CData<Object>
    
    when generating code for the equation of 'everywhere'
-}

module tests.comp.Issue277 where

import Data.Maybe

main = print $ invert [-1,0,1]

invert :: Data a => a -> a
invert = everywhere (mkT inv)
      where
          inv :: Int -> Int
          inv i = -i

-- from the original Data class in ghc and
-- https://github.com/rdegnan/typeable
everywhere :: 
              (forall a. Data a => a -> a)      -- this usedto provoke the compiler abort
           -- (forall x. Data x => x -> x)      -- replace a/x and it used to work correctly
           -> (forall a. Data a => a -> a)
everywhere f = f . gmapT (everywhere f)

mkT :: ( Typeable a
       , Typeable b
       )
    => (b -> b)
    -> a
    -> a
mkT = extT id

extT :: ( Typeable a
        , Typeable b
        )
     => (a -> a)
     -> (b -> b)
     -> a
     -> a
extT def ext = (T.unT) ((T def) `ext0` (T ext))

ext0 :: (Typeable a, Typeable b) => c a -> c b -> c a
ext0 def ext = maybe def id (gcast ext)

gcast :: (Typeable a, Typeable b) => c a -> Maybe (c b)
gcast x = r
 where
  unsafeCoerce = unsafeCoerce_
  r = if typeOf (getArg x) == typeOf (getArg (fromJust r))
        then Just $ unsafeCoerce x
        else Nothing
  getArg :: c x -> x
  getArg = undefined

pure native unsafeCoerce_ java.util.Objects.requireNonNull {a} :: a -> b

data T x = T { unT :: x -> x }
data ID x = ID { unID :: x }

instance Data a => Data [a] where
  gmapT  f   x = case x of
                      [] -> []
                      (y:ys) -> (f y:f ys)

instance Data Int

class Typeable a => Data a where
  gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
         -> (forall g. g -> c g)
         -> a
         -> c a
  gfoldl _ z = z
  gmapT :: (forall b. Data b => b -> b) -> a -> a
  gmapT f x0 = (ID.unID) (gfoldl (\(ID c) x -> ID (c (f x))) ID x0)

instance Typeable a => Typeable ([] a) where
  typeOf _ = "prelude.List.Int"
instance Typeable Int where
  typeOf _ = "prelude.Int"

class Typeable a where
  typeOf :: a -> String
